$\forall$${\it the\_es}$:ES, $e$:E, $l$:IdLnk, $m$:Msg, $i$:$\mathbb{N}$, $e_{1}$:E.
\\[0ex]($i$ $<$ $\parallel$sends($l$;$e$)$\parallel$)
\\[0ex]$\Rightarrow$ ($m$ = sends($l$;$e$)[$i$])
\\[0ex]$\Rightarrow$ ($\uparrow$isrcv($e_{1}$))
\\[0ex]$\Rightarrow$ (lnk($e_{1}$) = $l$)
\\[0ex]$\Rightarrow$ (tag($e_{1}$) = mtag($m$) $\in$ Id)
\\[0ex]$\Rightarrow$ (msgtype($m$) = valtype($e_{1}$) $\in$ Type)